Section: New Results

Automated Deduction

We develop general techniques which allow us to re-use available tools in order to build a new generation of solvers offering a good trade-off between expressiveness, flexibility, and scalability. We focus on the careful integration of combination techniques and rewriting techniques to design decision procedures for a wide range of verification problems. In his habilitation, Laurent Vigneron presents his contributions to the application of automated deduction for designing decision procedures and for verifying infinite systems, with a particular focus on abstract congruence closure and on verification of security protocols [17] .

Building and verifying decision procedures

Participants : Alain Giorgetti, Olga Kouchnarenko, Christophe Ringeissen, Elena Tushkanova.

We have developed a methodology to build decision procedures by using superposition calculi which are at the core of equational theorem provers. We are interested in developing automated deduction techniques to prove properties about these superposition-based decision procedures. To this aim, we plan to further investigate the use of meta-superposition, which has been already applied to check the termination and the combinability of superposition-based procedures [25] . We are working on the development of a framework for specifying and verifying superposition-based procedures. Since these procedures are defined as inference systems, we use the Maude system based on rewriting logic as a specification and prototyping language to implement superposition and meta-superposition.

Combining decision procedures

Participants : Christophe Ringeissen, Michaël Rusinowitch, Valerio Senni.

Modularity is a highly desirable property in the development of satisfiability procedures. In [59] we are interested in using a dedicated superposition calculus to develop satisfiability procedures for (unions of) theories sharing counter arithmetic. In the first place, we are concerned with the termination of this calculus for theories representing data structures and their extensions. To this purpose, we prove a modularity result for termination which allows us to use our superposition calculus as a satisfiability procedure for combinations of data structures. In addition, we present a general combinability result that permits us to use our satisfiability procedures into a non-disjoint combination method à la Nelson-Oppen without loss of completeness. This latter result is useful whenever data structures are combined with theories for which superposition is not applicable, like theories of arithmetic.